;;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: snark -*-
;;; File: assertion-file.lisp
;;; The contents of this file are subject to the Mozilla Public License
;;; Version 1.1 (the "License"); you may not use this file except in
;;; compliance with the License. You may obtain a copy of the License at
;;; http://www.mozilla.org/MPL/
;;;
;;; Software distributed under the License is distributed on an "AS IS"
;;; basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
;;; License for the specific language governing rights and limitations
;;; under the License.
;;;
;;; The Original Code is SNARK.
;;; The Initial Developer of the Original Code is SRI International.
;;; Portions created by the Initial Developer are Copyright (C) 1981-2006.
;;; All Rights Reserved.
;;;
;;; Contributor(s): Mark E. Stickel <stickel@ai.sri.com>.

(in-package :snark)

(defmacro in-language (language)
  (declare (ignore language))
  `(warn "Ignoring IN-LANGUAGE form."))

(defmacro in-kb (kb)
  ;; use suspend/resume for this?  okbc calls?
  (declare (ignore kb))
  `(warn "Ignoring IN-KB form."))

(defmacro has-author (author)
  `(setf *form-author* ',author))

(defmacro has-documentation (documentation)
  `(setf *form-documentation* ',documentation))

(defmacro has-name (name)
  `(setf *form-name* ',name))

(defmacro has-source (source)
  `(setf *form-source* ',source))

(declare-snark-option read-assertion-file-commands
                      '(assertion
                        has-author	;has-xxx specifies xxx for later assertions
                        has-documentation
                        has-name
                        has-source
                        in-package
                        in-language
                        in-kb
                        )		;every other form is an assertion
                      :never-print)

(declare-snark-option read-assertion-file-keywords
                      '((:author *form-author*)
                        (:documentation *form-documentation*)
                        (:name *form-name*)
                        (:source *form-source*))
                      :never-print)

(declare-snark-option read-assertion-file-format nil :never-print)
(declare-snark-option read-assertion-file-if-does-not-exist :error :never-print)
(declare-snark-option read-assertion-file-verbose nil :never-print)
(declare-snark-option read-assertion-file-package :snark-user :never-print)
(declare-snark-option read-assertion-file-readtable nil :never-print)
(declare-snark-option read-assertion-file-negate-conjectures nil :never-print)

(defun read-assertion-file (filespec
                            &key
                            (format (read-assertion-file-format?))
                            (if-does-not-exist (read-assertion-file-if-does-not-exist?))
                            (verbose (read-assertion-file-verbose?))
                            (package (or (read-assertion-file-package?) *package*))
                            (readtable (or (read-assertion-file-readtable?) *readtable*))
                            (negate-conjectures (read-assertion-file-negate-conjectures?))
                            hash-dollar)
  ;; read-asssertion-file executes commands and return a list of calls on 'assertion'
  ;; every form that is not a command (commands are named in (read-assertion-file-commands?))
  ;; is treated as a formula to be asserted
  (declare (ignorable verbose hash-dollar))
  (prog->
    (identity readtable -> *readtable*)
    (identity (read-assertion-file-commands?) -> commands)
    (identity (read-assertion-file-keywords?) -> keywords)
    (progv (mapcar #'second keywords)
           (consn nil nil (length keywords))
      (funcall (cond
                ((eq :tptp format)
                 'mapnconc-tptp-file-forms)
                (t
                 'mapnconc-file-forms))
               filespec
               :if-does-not-exist if-does-not-exist
               :package package
               ->* form)
      (and (consp form)
           (symbolp (first form))
           (first (member (first form) commands
                          :test #'string-equal		;command matching ignores package and case
                          :key #'symbol-name))
           -> command)
      (case command
        ((nil)
         (setf form (list 'assertion form)))
        (assertion
         (setf form (cons command (append (rest form) nil)))
         (setf command nil))
        (otherwise
         (eval (cons command (rest form)))))
      (unless command
        (case (and (consp form) (first form))
          (assertion
           (cond
            ((getf (cddr form) :ignore)
             nil)
            (t
             (when (and negate-conjectures (eq 'conjecture (getf (cddr form) :reason)))
               (setf (second form) (list 'not (second form)))
               (setf (getf (cddr form) :reason) 'negated_conjecture))
             (dolist (x keywords)
               (let ((v (symbol-value (second x))))
                 (when (and v (eq none (getf (cddr form) (first x) none)))
                   (nconc form (list (first x) v)))))
             (list form))))
          (otherwise
           (list form)))))))

(defun translate-assertion-file-to-tptp-format (inputfilespec &optional outputfilespec &rest read-assertion-file-options)
  (let ((snark-state (suspend-snark)))
    (unwind-protect
      (progn
        (initialize)
        (use-subsumption nil)
        (use-simplification-by-units nil)
        (use-simplification-by-equalities nil)
        (print-options-when-starting nil)
        (print-summary-when-finished nil)
        (print-rows-when-derived nil)
        (mapc #'eval (apply #'read-assertion-file inputfilespec read-assertion-file-options))
        (closure)
        (cond
         (outputfilespec
          (with-open-file (*standard-output* outputfilespec :direction :output)
            (print-rows :format :tptp)))
         (t
          (print-rows :format :tptp))))
      (resume-snark snark-state))
    nil))

(defun assertion-wff (x)
  (cond
   ((and (consp x)
         (eq 'assertion (car x))
         (consp (cdr x)))
    (second x))
   #+ignore
   ((and (consp x)
         (eq 'assert (car x))
         (consp (cdr x))
         (let ((x (second x)))
           (and (consp x)
                (eq 'quote (car x))
                (consp (cdr x))
                (null (cddr x)))))
    (warn "value ~S is not of the expected form (ASSERTION expr ...)." x)
    (second (second x)))
   (t
    (error "value ~S is not of the expected form (ASSERTION expr ...)." x))))

(declare-snark-option refute-file-initialize t :never-print)
(declare-snark-option refute-file-closure t :never-print)
(declare-snark-option refute-file-options nil :never-print)
(declare-snark-option refute-file-actions nil :never-print)
(declare-snark-option refute-file-ignore-errors nil :never-print)
(declare-snark-option refute-file-verbose t :never-print)
(declare-snark-option refute-file-output-file nil :never-print)
(declare-snark-option refute-file-if-exists nil :never-print)

(defun refute-file (filespec
                    &key
                    (initialize (refute-file-initialize?))
                    (closure (refute-file-closure?))
                    (format (read-assertion-file-format?))
		    (options (refute-file-options?))
                    (actions (refute-file-actions?))
                    (ignore-errors (refute-file-ignore-errors?))
		    (verbose (refute-file-verbose?))
                    (output-file (refute-file-output-file?))
                    (if-exists (refute-file-if-exists?))
                    (package (or (read-assertion-file-package?) *package*))
                    (readtable (or (read-assertion-file-readtable?) *readtable*)))
  (labels
    ((refute-file0 ()
       (when initialize
         (initialize))
       (mapc #'eval options)
       (mapc #'eval (funcall 'read-assertion-file filespec
                             :format format
                             :package package
                             :readtable readtable))
       (mapc #'eval actions)
       (when closure
         (or (closure) :done)))
     (refute-file1 ()
       (if verbose
           (print (time (refute-file0)))
           (refute-file0)))
     (refute-file2 ()
       (prog2
        (when verbose
          (format t "~&; Begin refute-file ~A " filespec) (print-current-time) (terpri))
        (if ignore-errors
            (mvlet (((:values value condition) (ignore-errors (refute-file1))))
              (or value (princ condition)))
            (refute-file1))
        (when verbose
          (format t "~&; End refute-file ~A "   filespec) (print-current-time) (terpri)))))
    (if output-file
        (with-open-file (stream output-file :direction :output :if-exists if-exists)
          (when stream
            (let ((*standard-output* stream) (*error-output* stream) (*trace-output* stream))
              (refute-file2))))
        (refute-file2))))

(defvar *tptp-input-directory*
  '(:absolute #+(and mcl (not openmcl)) "Haru" "Users" "mark" "tptp" "in"))

(defvar *tptp-output-directory*
  '(:absolute #+(and mcl (not openmcl)) "Haru" "Users" "mark" "tptp" "snark" "out"))

(defvar *tptp-problem-name-suffix* "")

(defun do-tptp-problem (problem &key (format (read-assertion-file-format?)) options)
  (let ((name (string problem)))
    (refute-file (make-pathname
                  :directory *tptp-input-directory*
                  :name (concatenate 'string name *tptp-problem-name-suffix*)
                  :type (if format (string-downcase (symbol-name format)) "kif"))
                 :format format
                 :options options
                 :ignore-errors t
                 :verbose t
                 :output-file (make-pathname
                               :directory *tptp-output-directory*
                               :name name
                               :type "out")
                 :if-exists nil)))

(defun do-tptp-problem1 (problem &key (format (read-assertion-file-format?)) options)
  (let ((name (string problem)))
    (refute-file (make-pathname
                  :directory *tptp-input-directory*
                  :name (concatenate 'string name *tptp-problem-name-suffix*)
                  :type (if format (string-downcase (symbol-name format)) "kif"))
                 :format format
                 :options (append '((use-hyperresolution t)
                                    (use-paramodulation t)
                                    (use-factoring :pos)
                                    (use-literal-ordering-with-hyperresolution 'literal-ordering-p)
                                    (use-literal-ordering-with-paramodulation  'literal-ordering-p)
				    (assert-context :current))
                                  options))))

;;; assertion-file.lisp EOF
